i:Id, ds1, ds2:x:Id fp Type, da:k:Knd fp Type, x, y:Id, T1, T2:Type, ks1, ks2:Knd List,
tr1:(k:{k:Knd| (k  ks1) }State(ds1)Valtype(da;k)T1T1),
tr2:(k:{k:Knd| (k  ks2) }State(ds2)Valtype(da;k)T2T2).
x = y
 ds1 || x : T1
 ds2 || y : T2
 ds2 || ds1  x : T1
 ds1 || ds2  y : T2
 R-state-var(i;ds1;da;x;T1;ks1;tr1) || R-state-var(i;ds2;da;y;T2;ks2;tr2) 

latex

Definitions	x:A. B(x), State(ds), P  Q, t  T, Top, S  T, S  T, x. t(x), P  Q, P  Q, P & Q, Prop, x(s), State(ds)
Lemmas	ma-state-subtype, fpf-sub-join-left2, fpf-sub weakening, ma-valtype wf, fpf-compatible-join-cap, fpf-cap-single1, subtype rel self, fpf-cap wf, top wf, decl-state wf, fpf-compatible wf, Id wf, id-deq wf, fpf-join wf, fpf-single wf, not wf, Knd wf, l member wf, fpf wf